#!/bin/bash
# usage: ./check_one.sh <spec_file> <property> <num_experiments> # <technique> (aborted)

SPEC=$1
PROPERTY=$2
NUM_EXPERIMENTS=$3
# TECH=$4

# 设置目录
SPEC_DIR="../dsn24"
LOG_DIR="../logs"
BYMC_DIR="/home/user/bymc/bymc"

# 检查日志目录是否存在，如果不存在则创建
if [ ! -d "$LOG_DIR" ]; then
    mkdir -p "$LOG_DIR"
    echo "Created log directory: $LOG_DIR"
fi

# if [ "$TECH" == 1 ]; then
#     CHECK="POPL17"
# elif [ "$TECH" == 2 ]; then
#     CHECK="CAV15"
# fi
# # 待运行的命令
# if [ "$TECH" == 1 ]; then
    COMMAND="$BYMC_DIR/verify $SPEC_DIR/$SPEC $PROPERTY -O schema.tech=ltl -O schema.incremental=1"
# elif [ "$TECH" == 2 ]; then
#     COMMAND="$BYMC_DIR/verify $SPEC_DIR/$SPEC $PROPERTY -O schema.tech=cav15"
# fi

# 遍历运行次数
for ((i = 1; i <= NUM_EXPERIMENTS; i++)); do
    # 获取当前时间作为日志文件名（确保不包含特殊字符）
    timestamp=$(date +"%Y-%m-%d_%H-%M-%S")
    timestamp="${timestamp//[^a-zA-Z0-9_-]/_}"  # 替换特殊字符为下划线
    # log_file="$LOG_DIR/"$SPEC"_"$PROPERTY"_"$CHECK"_run${i}_${timestamp}.log"
    log_file="$LOG_DIR/"$SPEC"_"$PROPERTY"_run${i}_${timestamp}.log"

    # 运行命令并将输出重定向到日志文件
    $COMMAND | tee "$log_file" 2>&1

    echo "Experiment $i completed. Log saved to $log_file"
done
